The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

sort#2(Nil) → Nil
sort#2(Cons(x4, x2)) → insert#3(x4, sort#2(x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x3, x2, x1) → Cons(x2, insert#3(x3, x1))
insert#3(x2, Nil) → Cons(x2, Nil)
insert#3(x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0, x8) → True
leq#2(S(x12), 0) → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x1) → sort#2(x1)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
sort#2(Cons(x4, x2)) →⁺ insert#3(x4, sort#2(x2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [x2 / Cons(x4, x2)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)